FDL - Nuprl Lemma : anti_sym_shift

Nuprl Lemma : anti_sym_shift

A, B:Type, R:(A

A

), S:(B

B

), f:(A

B).
Inj(A;B;f)

RelsIso(A;B;x,y.R(x,y);x,y.S(x,y);f)

AntiSym(B;x,y.S(x,y))

AntiSym(A;x,y.R(x,y))

Up gen algebra 1

Definitions of Statement RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f)

Definitions x,y. t(x;y), t T, AntiSym(T;x,y.R(x;y)), x(s1,s2), P Q, , x:A. B(x), RelsIso(T;T';x,y.R(x;y);x,y.R'(x;y);f), Inj(A;B;f), P & Q, P Q

Lemmas inject wf, rels iso wf, anti sym wf